\begin{tabbing}
$\forall$${\it es}$:ES.
\\[0ex](\=$\forall$$e$:E.\+
\\[0ex](timed)state after $e$
\\[0ex]=
\\[0ex]Trans(loc($e$))(kind($e$),val($e$),es\_state\_when(${\it es}$;$e$))
\\[0ex]$\in$ es\_state(${\it es}$;loc($e$)))
\-\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]($\uparrow$islocal(kind($e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$n$:$\mathbb{N}$\+
\\[0ex](($\uparrow$isl(Choose(loc($e$))(act(kind($e$)),$n$,(state when $e$))))
\\[0ex]c$\wedge$ (val($e$) = outl(Choose(loc($e$))(act(kind($e$)),$n$,(state when $e$))) $\in$ valtype($e$)))))
\-\-\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]($\uparrow$isrcv(kind($e$)))
\\[0ex]$\Rightarrow$ ($<$lnk(kind($e$)), tag(kind($e$)), val($e$)$>$ $\in$ \=Send(loc(sender($e$)))\+
\\[0ex](kind(sender($e$))
\\[0ex],val(sender($e$))
\\[0ex],(state when sender($e$)))))
\-\-
\end{tabbing}